Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
b(a(a(b(a(x1))))) → a(b(a(a(b(b(a(a(b(x1)))))))))
Q is empty.
↳ QTRS
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
b(a(a(b(a(x1))))) → a(b(a(a(b(b(a(a(b(x1)))))))))
Q is empty.
We have reversed the following QTRS:
The set of rules R is
b(a(a(b(a(x1))))) → a(b(a(a(b(b(a(a(b(x1)))))))))
The set Q is empty.
We have obtained the following QTRS:
a(b(a(a(b(x))))) → b(a(a(b(b(a(a(b(a(x)))))))))
The set Q is empty.
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ RFCMatchBoundsTRSProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(a(b(x))))) → b(a(a(b(b(a(a(b(a(x)))))))))
Q is empty.
Termination of the TRS R could be shown with a Match Bound [6,7] of 2. This implies Q-termination of R.
The following rules were used to construct the certificate:
a(b(a(a(b(x))))) → b(a(a(b(b(a(a(b(a(x)))))))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
152, 153, 160, 161, 157, 158, 156, 154, 159, 155, 168, 169, 165, 166, 164, 162, 167, 163, 176, 177, 173, 174, 172, 170, 175, 171, 184, 185, 181, 182, 180, 178, 183, 179, 192, 193, 189, 190, 188, 186, 191, 187
Node 152 is start node and node 153 is final node.
Those nodes are connect through the following edges:
- 152 to 154 labelled b_1(0)
- 153 to 153 labelled #_1(0)
- 160 to 161 labelled b_1(0)
- 161 to 153 labelled a_1(0)
- 161 to 162 labelled b_1(1)
- 157 to 158 labelled b_1(0)
- 158 to 159 labelled a_1(0)
- 158 to 170 labelled b_1(1)
- 156 to 157 labelled b_1(0)
- 154 to 155 labelled a_1(0)
- 159 to 160 labelled a_1(0)
- 159 to 162 labelled b_1(1)
- 155 to 156 labelled a_1(0)
- 168 to 169 labelled b_1(1)
- 169 to 153 labelled a_1(1)
- 169 to 162 labelled b_1(1)
- 165 to 166 labelled b_1(1)
- 166 to 167 labelled a_1(1)
- 166 to 178 labelled b_1(2)
- 164 to 165 labelled b_1(1)
- 162 to 163 labelled a_1(1)
- 167 to 168 labelled a_1(1)
- 167 to 162 labelled b_1(1)
- 163 to 164 labelled a_1(1)
- 176 to 177 labelled b_1(1)
- 177 to 165 labelled a_1(1)
- 177 to 186 labelled b_1(2)
- 173 to 174 labelled b_1(1)
- 174 to 175 labelled a_1(1)
- 172 to 173 labelled b_1(1)
- 170 to 171 labelled a_1(1)
- 175 to 176 labelled a_1(1)
- 171 to 172 labelled a_1(1)
- 184 to 185 labelled b_1(2)
- 185 to 165 labelled a_1(2)
- 185 to 186 labelled b_1(2)
- 181 to 182 labelled b_1(2)
- 182 to 183 labelled a_1(2)
- 180 to 181 labelled b_1(2)
- 178 to 179 labelled a_1(2)
- 183 to 184 labelled a_1(2)
- 179 to 180 labelled a_1(2)
- 192 to 193 labelled b_1(2)
- 193 to 169 labelled a_1(2)
- 193 to 178 labelled b_1(2)
- 189 to 190 labelled b_1(2)
- 190 to 191 labelled a_1(2)
- 190 to 178 labelled b_1(2)
- 188 to 189 labelled b_1(2)
- 186 to 187 labelled a_1(2)
- 191 to 192 labelled a_1(2)
- 191 to 162 labelled b_1(1)
- 187 to 188 labelled a_1(2)